;;; -*- Mode: LISP; Package: USER; Base: 10 -*-

(HERALD EVENTS)

(DEFEVENT ADD-AXIOM (NAME TYPES TERM)
  (LET ((IN-ADD-AXIOM-FLG T))
    (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	   (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE ADD-AXIOM)
						NAME TYPES TERM))
				    T
				    (QUOTE C)
				    NIL T T)))
	  (T (LET (MAIN-EVENT-NAME)
	       (CHK-ACCEPTABLE-LEMMA NAME TYPES TERM)
	       (MAKE-EVENT NAME (LIST (QUOTE ADD-AXIOM) NAME TYPES TERM))
	       (ADD-FACT NIL (QUOTE NONCONSTRUCTIVE-AXIOM-NAMES)
			 NAME)
	       (ADD-LEMMA0 NAME TYPES TERM)
	       (DEPEND NAME (ALL-FNNAMES (TRANSLATE TERM)))
	       NAME)))))

(DEFEVENT ADD-SHELL
  (SHELL-NAME BTM-FN-SYMB RECOGNIZER DESTRUCTOR-TUPLES)
  (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	 (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE ADD-SHELL)
					      SHELL-NAME BTM-FN-SYMB
					      RECOGNIZER
					      DESTRUCTOR-TUPLES))
				  T (QUOTE C) NIL T T)))
	(T (LET (MAIN-EVENT-NAME)
	     (CHK-ACCEPTABLE-SHELL SHELL-NAME BTM-FN-SYMB RECOGNIZER
				   DESTRUCTOR-TUPLES)
	     (MAKE-EVENT SHELL-NAME
			 (LIST (QUOTE ADD-SHELL)
			       SHELL-NAME BTM-FN-SYMB RECOGNIZER
			       DESTRUCTOR-TUPLES))
	     (ADD-SHELL0 SHELL-NAME BTM-FN-SYMB RECOGNIZER
			 DESTRUCTOR-TUPLES)
	     (DEPEND SHELL-NAME
		     (SET-DIFF (UNION (LOOP FOR X IN DESTRUCTOR-TUPLES
					    WITH LOOP-ANS
					    DO (SETQ LOOP-ANS
						     (UNION (CDR (CADR X))
							    LOOP-ANS))
					    FINALLY (RETURN LOOP-ANS))
				      (LOOP FOR X IN DESTRUCTOR-TUPLES
					    WITH LOOP-ANS
					    DO
					    (SETQ LOOP-ANS
						  (ADD-TO-SET (CADDR X)
							      LOOP-ANS))
					    FINALLY (RETURN LOOP-ANS)))
			       (COND (BTM-FN-SYMB (LIST BTM-FN-SYMB
							RECOGNIZER))
				     (T (LIST RECOGNIZER)))))

;   Make the shell depend on every fn used in the type restrictions and
;   defaults except the BTM-FN-SYMB and RECOGNIZER of this type.

	     SHELL-NAME))))

(DEFUN BOOT-STRAP ()
    (LET ((IN-BOOT-STRAP-FLG T))
    (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	(CAR (REDO-UNDONE-EVENTS
	      (LIST (LIST (QUOTE BOOT-STRAP)))
	      T
	      (QUOTE C)
	      NIL
	      T
	      T)))
      (T (LET (MAIN-EVENT-NAME
	       (ARITY-ALIST
		(QUOTE ((NOT . 1) (AND . 2) (OR . 2) (IMPLIES . 2)
				  (LESSP . 2) (PLUS . 2)))))
	   (BOOT-STRAP0)
	   (MAKE-EVENT (QUOTE GROUND-ZERO) (LIST (QUOTE BOOT-STRAP)))
	   (ADD-FACT (QUOTE IF) (QUOTE LISP-CODE) (QUOTE 1IF))
	   (ADD-FACT (QUOTE EQUAL) (QUOTE LISP-CODE) (QUOTE 1EQUAL))
	   (ADD-FACT (QUOTE IF)
		     (QUOTE TYPE-PRESCRIPTION-LST)
		     (CONS (QUOTE GROUND-ZERO)
			   (QUOTE (0 NIL T T))))
	   (ADD-FACT (QUOTE EQUAL)
		     (QUOTE TYPE-PRESCRIPTION-LST)
		     (CONS (QUOTE GROUND-ZERO)
			   (CONS TYPE-SET-BOOLEAN (QUOTE (NIL NIL)))))
	   (ADD-FACT (QUOTE COUNT) (QUOTE LISP-CODE) (QUOTE 1COUNT))
	   (ADD-FACT (QUOTE COUNT)
		     (QUOTE TYPE-PRESCRIPTION-LST)
		     (CONS (QUOTE GROUND-ZERO)
			   (CONS TYPE-SET-NUMBERS (QUOTE (NIL)))))
	   (LOOP FOR INSTR IN BOOT-STRAP-INSTRS DO (APPLY (CAR INSTR)
							  (CDR INSTR)))
	   (SETQ FAILED-THMS NIL)
	   (QUOTE GROUND-ZERO))))))

(DEFEVENT DCL (NAME ARGS)
  (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	 (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE DCL)
					      NAME ARGS))
				  T
				  (QUOTE C)
				  NIL T T)))
	(T (LET (MAIN-EVENT-NAME)
	     (CHK-ACCEPTABLE-DCL NAME ARGS)
	     (MAKE-EVENT NAME (LIST (QUOTE DCL) NAME ARGS))
	     (DCL0 NAME ARGS)
	     NAME))))

(DEFEVENT DEFN (NAME ARGS BODY RELATION-MEASURE-LST)
  (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	 (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE DEFN)
					      NAME ARGS BODY
					      RELATION-MEASURE-LST))
				  T
				  (QUOTE C)
				  NIL T T)))
	(T
	 (LET (MAIN-EVENT-NAME)
	   (CHK-ACCEPTABLE-DEFN NAME ARGS BODY RELATION-MEASURE-LST)
	   (MAKE-EVENT NAME (COND (RELATION-MEASURE-LST
				   (LIST (QUOTE DEFN) NAME ARGS BODY
					 RELATION-MEASURE-LST))
				  (T (LIST (QUOTE DEFN) NAME ARGS BODY))))
	   (DEFN0 NAME ARGS BODY RELATION-MEASURE-LST NIL)
	   (DEPEND
	    NAME
	    (REMOVE
	     NAME
	     (UNION
	      (ALL-FNNAMES (TRANSLATE BODY))
	      (UNION
	       ALL-LEMMAS-USED
	       (LOOP FOR TEMP IN (GET1 NAME (QUOTE JUSTIFICATIONS))
		     WITH LOOP-ANS
		     DO (SETQ
			 LOOP-ANS
			 (UNION (COND
				 ((NULL (ACCESS JUSTIFICATION RELATION TEMP))
				  NIL)
				 (T (UNION (ALL-FNNAMES (ACCESS
							 JUSTIFICATION
							 MEASURE-TERM
							 TEMP))
					   (ADD-TO-SET (ACCESS JUSTIFICATION
							       RELATION TEMP)
						       (ACCESS JUSTIFICATION
							       LEMMAS TEMP)))))
				LOOP-ANS))
		     FINALLY (RETURN LOOP-ANS))))))
	   (PRINT-DEFN-MSG NAME ARGS)
	   (DEFN-WRAPUP (TOTAL-FUNCTIONP NAME))
	   (COND ((TOTAL-FUNCTIONP NAME)
		  NAME)
		 (T NIL))))))

(DEFEVENT DISABLE (OLDNAME)
  (APPLY (FUNCTION TOGGLE) (LIST (MAKE-NEW-NAME) OLDNAME T)))

(DEFEVENT ENABLE (OLDNAME)
  (APPLY (FUNCTION TOGGLE) (LIST (MAKE-NEW-NAME) OLDNAME NIL)))

(DEFEVENT PROVE-LEMMA (NAME TYPES TERM HINTS)
  (LET ((IN-PROVE-LEMMA-FLG T))
    (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	   (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE PROVE-LEMMA)
						NAME TYPES TERM HINTS))
				    T
				    (QUOTE C)
				    NIL T T)))
	  (T
	   (LET (PROVE-ANS MAIN-EVENT-NAME)
	     (CHK-ACCEPTABLE-LEMMA NAME TYPES TERM)
	     (CHK-ACCEPTABLE-HINTS HINTS)
	     (UNWIND-PROTECT
	       (PROGN

;   Before calling PROVE we call APPLY-HINTS.  APPLY-HINTS sets some global
;   variables that affect the theorem-prover.  We enter an UNWIND-PROTECT here
;   so that we can set those variables to their standard default values no
;   matter how we exit PROVE.

		 (SETQ PROVE-ANS
		       (PROVE (APPLY-HINTS HINTS TERM)))
		 (COND (PROVE-ANS
			(MAKE-EVENT NAME (COND (HINTS
						(LIST (QUOTE PROVE-LEMMA)
						      NAME TYPES TERM HINTS))
					       (T (LIST (QUOTE PROVE-LEMMA)
							NAME TYPES TERM))))
			(ADD-LEMMA0 NAME TYPES TERM)
			(DEPEND NAME
				(UNION ALL-LEMMAS-USED
				       (UNION (EXTRACT-DEPENDENCIES-FROM-HINTS
						HINTS)
					      (ALL-FNNAMES
					       (TRANSLATE TERM)))))))
		 (COND (PROVE-ANS NAME)
		       (T NIL)))
	       (LOOP FOR X IN HINT-VARIABLE-ALIST
		     DO (SET (CADR X) (CADDDR X)))))))))

(DEFEVENT REFLECT (NAME SATISFACTION-LEMMA-NAME RELATION-MEASURE-LST)
  (COND
    ((NOT IN-REDO-UNDONE-EVENTS-FLG)
     (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE REFLECT)
					  NAME
					  SATISFACTION-LEMMA-NAME
					  RELATION-MEASURE-LST))
			      T
			      (QUOTE C)
			      NIL T T)))
    (T
     (LET (MAIN-EVENT-NAME)
       (DEFN-SETUP (LIST (QUOTE REFLECT)
			 NAME SATISFACTION-LEMMA-NAME
			 RELATION-MEASURE-LST))
       (CHK-ACCEPTABLE-REFLECT NAME SATISFACTION-LEMMA-NAME
			       RELATION-MEASURE-LST)
       (MAKE-EVENT NAME
		   (COND (RELATION-MEASURE-LST
			  (LIST (QUOTE REFLECT) NAME SATISFACTION-LEMMA-NAME
				RELATION-MEASURE-LST))
			 (T (LIST (QUOTE REFLECT) NAME
				  SATISFACTION-LEMMA-NAME))))
       (REFLECT0 NAME SATISFACTION-LEMMA-NAME
		 RELATION-MEASURE-LST NIL)
       (DEPEND
	 NAME
	 (REMOVE
	   NAME
	   (ADD-TO-SET
	     SATISFACTION-LEMMA-NAME
	     (UNION-EQUAL
	       ALL-LEMMAS-USED
	       (LOOP FOR TEMP IN (GET1 NAME (QUOTE JUSTIFICATIONS))
		     WITH LOOP-ANS
		     DO (SETQ LOOP-ANS
			      (UNION
				(COND
				  ((NULL (ACCESS JUSTIFICATION RELATION TEMP))
				   NIL)
				  (T (UNION (ALL-FNNAMES (ACCESS
							   JUSTIFICATION
							   MEASURE-TERM
							   TEMP))
					    (ADD-TO-SET (ACCESS JUSTIFICATION
								RELATION TEMP)
							(ACCESS
							 JUSTIFICATION
							 LEMMAS TEMP)))))
				LOOP-ANS))
		     FINALLY (RETURN LOOP-ANS))))))
       (PRINT-DEFN-MSG NAME (CADR (GET1 NAME (QUOTE SDEFN))))
       (DEFN-WRAPUP (TOTAL-FUNCTIONP NAME))
       (COND ((TOTAL-FUNCTIONP NAME)
	      NAME)
	     (T NIL))))))

(DEFEVENT TOGGLE (NAME OLDNAME FLG)
  (COND ((NOT IN-REDO-UNDONE-EVENTS-FLG)
	 (CAR (REDO-UNDONE-EVENTS (LIST (LIST (QUOTE TOGGLE)
					      NAME OLDNAME FLG))
				  T
				  (QUOTE C)
				  NIL T T)))
	(T (LET (MAIN-EVENT-NAME)
	     (CHK-ACCEPTABLE-TOGGLE NAME OLDNAME FLG)
	     (MAKE-EVENT NAME (LIST (QUOTE TOGGLE) NAME OLDNAME FLG))
	     (ADD-FACT NIL (QUOTE DISABLED-LEMMAS)
		       (CONS OLDNAME (CONS NAME FLG)))
	     (DEPEND NAME (LIST (MAIN-EVENT-OF OLDNAME)))
	     NAME))))